(declare-fun e () Real)
(declare-fun g () Real)
(declare-fun h () Real)
(declare-fun k () Real)
(declare-fun c () Real)
(declare-fun n () Real)
(declare-fun a () Real)
(declare-fun j () Real)
(declare-fun r () Real)
(declare-fun f () Real)
(declare-fun l () Real)
(declare-fun s () Real)
(declare-fun d () Real)
(declare-fun u () Real)
(declare-fun m () Real)
(declare-fun o () Real)
(declare-fun p () Real)
(declare-fun b () Real)
(declare-fun aa () Real)
(declare-fun q () Real)
(declare-fun ab () Real)
(declare-fun t () Real)
(assert (forall ((i Real)) (let ((v (and (= m g) (= l (/ 0 u)) (distinct (/ d s) 1.0)))(w (or (< 0.0 i) (>= i (- c))))(x (> 0.0 (* (/ 0.0 k) h)))) (and (or v (>= (/ 3.0 k) l) (<= (/ f r) 0.0)) (> j g) (< 0.0 (/ a n)) (> 0.0 g) w (or x (< (- h) g) (< 0.0 e))))))
(assert (exists ((c Real)) (let ((v (>= (/ 5.0 b m) n o))(w (/ (* ab g (/ 0 g)) p))(x (- (+ (/ 166.0 aa h) (* 5.0 r r)) (- (- 250.0 (/ 100.0 r)) (+ 120.0 b))))(y (+ 115.0 (/ 155.0 (+ 199.0 aa h) (- 197.0 r r)) (/ (* 2.0 r) (/ 253.0 b m)) (- 73.0 q)))(z (* (+ (/ 8.0 aa h) r) b m))) (let ((ac (>= o (* 29.0 123.0 (- (+ x 24.0 q)))))(ad (/ (* (/ 8.0 (- h)) b m) z))) (let ((ae (>= (/ 3.5 y (* ad p)) o))) (or (and (or (> 0.0 r) v) (>= w (/ aa h))) (and ac ae)))))))
(assert (distinct b (+ m t g)))
(check-sat)
